package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class ToyS1 {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("ToyS1");
		 
         // Variables
		 TypedData x = new TypedData("x", Constants.TYPE_INTEGER);
		 tiosts.addVariable(x);
         
         // There are no parameters       
         
         Action init1 = new Action("Init1", Constants.ACTION_INTERNAL);
         tiosts.addAction(init1);
         Action b = new Action("b", Constants.ACTION_INPUT);
         tiosts.addAction(b);
         tiosts.addActionParameter(x);
         Action a = new Action("a", Constants.ACTION_OUTPUT);
         tiosts.addAction(a);         
         
         Location start1 = new Location("Start1");
         tiosts.addLocation(start1);
         Location s0 = new Location("S0");
         tiosts.addLocation(s0);
         Location s1 = new Location("S1");
         tiosts.addLocation(s1);        
         Location s2 = new Location("S2");
         tiosts.addLocation(s2);
         Location lc1 = new Location("lc1");
         tiosts.addLocation(lc1);
         
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start1);
         
         // Transitions
         tiosts.createTransition("Start1", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init1, null, null, "S0");
         tiosts.createTransition("S0", Constants.GUARD_TRUE, Constants.GUARD_TRUE, b, "x := 0", null, "S1");
         tiosts.createTransition("S1", "x < 5", Constants.GUARD_TRUE, a, null, null, "S2");
         tiosts.createTransition("S1", Constants.GUARD_TRUE, Constants.GUARD_TRUE, b, null, null, "lc1");
         tiosts.createTransition("S2", Constants.GUARD_TRUE, Constants.GUARD_TRUE, b, null, null, "lc1");
         
         return tiosts;		 
	 }

}
